%evaluation
With the goal of finding evidences of bad smells appearing in contracts, we tried to detect their characterization in systems with considerable use of contracts. We began by observing graduate students in medium-sized projects -- we provide an account of the experience in Section~\ref{sect:students}. They had little experience in formal methods. In another experiment, we analyzed whether contracts written by more experienced developers have similar smells. Some classes annotated with contracts from the JML models API were used -- Section~\ref{sect:api} shows the results.

\subsection{JML Student Projects}
\label{sect:students}

%the motivation for this work - class 
The first idea of gathering bad smells initially developed from observing five graduate student projects for JML-based subjects at University of Pernambuco (Brazil) in the Systems Specification and Verification course. Targeting at diverse application domains, students had to write contracts and code from previously elicited requirements, during three small iterations. Requirements were modelled by using Alloy~\cite{alloy-book-published} as a formal specification language.

In the first iteration, we observed that students complained mostly about JML syntax -- they had never experienced the language or DBC --, but the source code did not present noticeable issues regarding encapsulation and readability. Some projects did not properly apply model fields for implementing abstract concepts, thus the \emph{Open Doors} smell was often found in initial versions of these projects.

In later iterations, students had to evolve previously written contracts, in order to acommodate modifications from changing requirements. This scenario is commonly seen in real project settings, so likely to occur if DBC is used in such context. Contract maintenance became more difficult as the end of the projects drew near; some smells were more recurrent, such as \emph{Open Doors}, \emph{Long Specs}, \emph{Field Obsession} and \emph{Illogical Contracts}. Results from these projects originated most smells from our catalog.


\subsection{JML models API Analysis}
\label{sect:api}

%JML models API
Greater evidence of how often the smells can appear in applications was found when we analyzed the JML models API source code~\cite{jml-models-api}. Classes of this API offer ample spectre of specifications. 
%how big it is
For instance, a single class -- \code{JMLEqualsSequence} -- contains more than 1,600 lines of specification code. The classes were developed by experienced JML developers (some of them are JML pioneers), and they certainly constitute one of the richest available sources of contracts, considering open source systems. Currently, most well-designed DBC applications with JML employ classes from this API in contracts, showing its substantial importance.

%methodology
The API offers classes for abstract specifications, as they emulate mathematical objects (such as sets, bags and sequences). It includes more than one hundred classes and interfaces, all of them containing JML contracts. From this API, Collection objects are equally divided in Object, Value and Equals collections. Object collections treats components as object references, while Value collections have values, for which any inserted object is cloned from the original reference. Equals collections are hybrid, using the Java \code{equals} methods. The API also offers classes that represent Relations and Maps~\cite{jml-reference}. For our analysis, with the intent of analyzing a representative subset of classes, we chose -- with no previous inspection -- one API class for each of the following categories:
\begin{itemize}
	\item basic type: \code{JMLChar};
	\item composite type: \code{JMLString};
	\item object collection: \code{JMLObjectSet};
	\item value collection: \code{JMLValueBag};
	\item equals collection: \code{JMLEqualsSequence};
	\item interface: \code{JMLCollection};
	\item relation: \code{JMLEqualsToEqualsRelation}.
\end{itemize}

%justification - API isn't made for DBC

%results
These six classes are representative in the sense that other classes present very similar specifications for different types, therefore the same smells are likely to be detected. From manual detection of bad smells in the selected classes, the results are showed in Table~\ref{tab:results}. These numbers are \emph{our interpretation} of the analyzed specifications, under the DBC perspective. Developers of the API aim at complete mathematical specifications (which they call ``equational reasoning''), not DBC development. Still, developers must inspect these specifications in order to gain deep understand of the API services, thus avoiding bad smells can be relevant.


\begin{table*}[ht]
  \centering
  \caption{Case study results}
  \scalebox{0.8}{
    \begin{tabular}{|l|c|l|} \hline   
    {\bf Classes from the API } & \parbox{1.5cm}{{\bf Approx. contract size (LOC)}} & {\bf Detected smells } \\ \hline
    JMLChar  & 155 & \emph{Long Specs}  \\ \hline
    JMLString  & 105 & \emph{Long Specs} \\ \hline
    JMLObjectSet  & 508 & \parbox{5cm}{\emph{Open Doors, Specification Overkill, Long Specs}} \\ \hline
    JMLValueBag  & 821 & \parbox{5cm}{\emph{Open Doors, Field Obsession, Specification Overkill, Long Specs, Illogical Contracts, Purely Nothing}}  \\ \hline
    JMLEqualsSequence  & 1,600 & \parbox{5cm}{\emph{Long Specs, Illogical Contracts}} \\ \hline
    JMLEqualstoEqualsRelation  & 645 & \emph{Long Specs} \\ \hline
    JMLCollection  & 44 & -  \\ \hline
    \end{tabular}}
  \label{tab:results}
\end{table*}


%comments about the results
%numbers
The number of detected bad smells is proportional to the class size, which is not surprising, since smells are more frequent in bigger contracts. In JML, due to its use of Java expressions, more complex predicates tend to become expressions of several lines long.
%not all bad smells from catalog - some are more common
Further on the results, some of the catalogued smells were not found. On the other hand, other smells are recurrent: \emph{Long Specs}, \emph{Illogical Contracts} and \emph{Open Door}s. We believe that these smells and their variations are the most commonly found in practice (the same result was observed in our students' projects).

%explore bag class (code fragments)
From the selected classes, \code{JMLValueBag} happens to exhibit more smells than any other. For instance, the protected field \code{size} is made available to contracts by \code{\textbf{spec\_public}}. Fields in this class are constants, since the JML mathematical types are immutable~\cite{jml-models-api}.

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
public /*@ pure @*/ class JMLValueBag 
	extends JMLValueBagSpecs implements JMLCollection{..
	
	protected final JMLValueBagEntryNode the_list; ..
	protected /*@ spec_public @*/ final int size;

  //@ public invariant size >= 0; ..

\end{lstlisting} 

Exemplars of \emph{Field Obsession} are seen in method postconditions, for instance with the \code{getMatchingEntry}. This method, which declares non-pure methods that have no assignable clause, also present the \emph{Purely Nothing} smell.

\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
		/*@  assignable \nothing;
      @  ensures the_list==null ==> 
      @      \result == null;
      @  ensures \result != null ==> 
      @		   0<=\result.count && 
      @      \result.count<=size;
      @*/
    protected JMLValueBagEntry getMatchingEntry(JMLType item){..}
\end{lstlisting} 

Instances of \emph{Long Specs} and \emph{Specification Overkill} are found in some method contracts, as in \code{convertFrom}.
\begin{lstlisting}[frame=single,framerule=0pt,numbers=none]
	/*@ public normal_behavior
    @    requires a != null;
    @    ensures \result != null &&
    @        \result.int_size()==a.length;
    @    ensures_redundantly \result!=null && 		
    @				\result.int_size()==a.length &&
    @       (\forall int i;
    @         0<=i && i<a.length;
    @       	\result.has(a[i])
    @       );
    @*/
    public static JMLValueBag convertFrom(JMLType[] a){..}
\end{lstlisting} 

%the study is not conclusive - very simple purpose
Our intent with this evaluation was only to provide evidence that smells are present in applications with contracts in JML. Still, experiments must be carried out in order to point out the most frequent smells and reason about causes that lead to smells in DBC code.
